package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Mouse {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Mouse");
		 
		 //Clocks
		 tiosts.addClock("clockM");
		 
         // Variables
         TypedData coordinateM = new TypedData("coordinateM", Constants.TYPE_INTEGER);
         tiosts.addVariable(coordinateM);
         
         // Parameters
         TypedData position = new TypedData("position", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(position);
         
         // Input, output, and internal actions
         Action init = new Action("initM", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         Action click = new Action("click", Constants.ACTION_INPUT);
         click.addParameter(position.getName());
         tiosts.addAction(click);
         Action simpleClick = new Action("simpleClick", Constants.ACTION_OUTPUT);
         simpleClick.addParameter(position.getName());
         tiosts.addAction(simpleClick);
         Action doubleClick = new Action("doubleClick", Constants.ACTION_OUTPUT);
         doubleClick.addParameter(position.getName());
         tiosts.addAction(doubleClick);
         
         // Locations
         Location start = new Location("StartM");
         tiosts.addLocation(start);
         Location s0 = new Location("S0");
         tiosts.addLocation(s0);
         Location s1 = new Location("S1");
         tiosts.addLocation(s1);    
         Location s2 = new Location("S2");
         tiosts.addLocation(s2);  
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("StartM", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S0");
         tiosts.createTransition("S0",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, click, "coordinateM := position", null, Constants.DEADLINE_LAZY, "S1");
         tiosts.createTransition("S1",  Constants.GUARD_TRUE, "clockM <= 2", click, "coordinateM := position", null, Constants.DEADLINE_LAZY, "S2");
         tiosts.createTransition("S2", "coordinateM = position", Constants.GUARD_TRUE, doubleClick, null, "clockM := 0", Constants.DEADLINE_DELAYABLE, "S0");
         tiosts.createTransition("S1", "coordinateM = position", "clockM > 2", simpleClick, null, "clockM := 0", Constants.DEADLINE_EAGER, "S0");
         
         return tiosts;		 
	 }

}
